es-first-at-since(es;i;e;e.R(e);e.P(e))
== loc(e) = i
== & P(e) & (R(e))
== & (e'<e. P(e')  (e'':E. (e' loc e''  & (e'' <loc e) & R(e'')))) 

latex

---

clarification:

es-first-at-since(es;i;e;e.R(e);e.P(e))
== es-loc(es; e) = i  Id
== & P(e) & (R(e))
== & alle-lt(es;e;e'.P(e')
== &  (e'':es-E(es). (es-le(es;e';e'') & es-locl(es; e''; e) & R(e'')))) 

latex

Definitions	es-first-at-since(es;i;e;e.R(e);e.P(e)), Id, loc(e), A, e<e'. P(e), P  Q, x:A. B(x), E, e loc e' , P & Q, (e <loc e')
FDL editor aliases	es-first-at-since